Termination proof of /tmp/tmpBUWy26/Count.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 DuplicateArgsRemoverProof (⇔)

        ↳7 ITRS

        ↳8 ITRStoIDPProof (⇔)

        ↳9 IDP

        ↳10 UsableRulesProof (⇔)

        ↳11 IDP

        ↳12 ItpfGraphProof (⇔)

        ↳13 IDP

        ↳14 IDPtoQDPProof (⇐)

        ↳15 QDP

        ↳16 UsableRulesProof (⇔)

        ↳17 QDP

        ↳18 QReductionProof (⇔)

        ↳19 QDP

        ↳20 QDPOrderProof (⇔)

        ↳21 QDP

        ↳22 DependencyGraphProof (⇔)

        ↳23 QDP

        ↳24 UsableRulesProof (⇔)

        ↳25 QDP

        ↳26 QReductionProof (⇔)

        ↳27 QDP

        ↳28 QDPOrderProof (⇔)

        ↳29 QDP

        ↳30 DependencyGraphProof (⇔)

        ↳31 AND

            ↳32 QDP

                ↳33 QDPOrderProof (⇔)

                ↳34 QDP

                ↳35 QDPOrderProof (⇔)

                ↳36 QDP

                ↳37 DependencyGraphProof (⇔)

                ↳38 TRUE

            ↳39 QDP

                ↳40 QDPOrderProof (⇔)

                ↳41 QDP

                ↳42 QDPOrderProof (⇔)

                ↳43 QDP

                ↳44 DependencyGraphProof (⇔)

                ↳45 TRUE

    ↳46 ITRS

        ↳47 DuplicateArgsRemoverProof (⇔)

        ↳48 ITRS

        ↳49 ITRSFilterProcessorProof (⇐)

        ↳50 ITRS

        ↳51 ITRSFSMergerProof (⇐)

        ↳52 ITRS

        ↳53 ITRStoIDPProof (⇔)

        ↳54 IDP

        ↳55 UsableRulesProof (⇔)

        ↳56 IDP

        ↳57 ItpfGraphProof (⇔)

        ↳58 IDP

        ↳59 IDPNonInfProof (⇐)

        ↳60 AND

            ↳61 IDP

                ↳62 IDependencyGraphProof (⇔)

                ↳63 TRUE

            ↳64 IDP

                ↳65 IDependencyGraphProof (⇔)

                ↳66 TRUE

(0) Obligation:

JBC Problem based on JBC Program:

No human-readable program information known.

Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: Count

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 698 nodes with 2 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Complex Obligation (AND)

(5) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load1265(o831, o830, i130) → NULL1315(o831, o830, i130, o830)
NULL1315(o859, java.lang.Object(Tree(java.lang.Object(Tree(o996Field0, o996Field1, o996Field2)), o944, o945)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o996Field0, o996Field1, o996Field2)), o944, o945))) → Load21911(o859, java.lang.Object(Tree(java.lang.Object(Tree(o996Field0, o996Field1, o996Field2)), o944, o945)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o996Field0, o996Field1, o996Field2)), o944, o945)), java.lang.Object(Tree(java.lang.Object(Tree(o996Field0, o996Field1, o996Field2)), o944, o945)), NULL)
Store26273(o16609, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o18621, o18622, o18623)), o17126, o17127)), o16604, o18621) → Load21911(o16609, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(o18621, java.lang.Object(Tree(o18622, o17126, NULL)), NULL)), o16604)
Load21911(o16609, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o18621, o18622, o18623)), o17126, o17127)), o16604) → Load21911(o16609, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(o18621, java.lang.Object(Tree(o18622, o17126, NULL)), NULL)), o16604)
Load21911(o16609, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(NULL, o17126, o17127)), o16604) → Load21911(o16609, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), o17126, java.lang.Object(Tree(NULL, o16604, NULL)))
Load21911(o16609, java.lang.Object(Tree(java.lang.Object(Tree(o17786, o17787, o17788)), o16607, o16608)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o17786, o17787, o17788)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o17786, o17787, o17788)), o16607, o16608)), o16604) → Load21911(o16609, java.lang.Object(Tree(java.lang.Object(Tree(o17786, o17787, o17788)), o16607, o16608)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o17786, o17787, o17788)), o16607, o16608)), java.lang.Object(Tree(o17786, java.lang.Object(Tree(o17787, o16607, NULL)), NULL)), o16604)
Load21911(o16609, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o19480, o19481, o19482)), o17126, o17127)), o16604) → Store26273(o16609, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o19480, o19481, o19482)), o17126, o17127)), o16604, o19480)
Load22061(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), NULL, o16669) → JMP22682(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), o16669, i141)
JMP22682(o16609, o16604, i141) → Load1265(o16609, o16604, i141)
Load21911(o16609, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), NULL, o16604) → Load1265(o16609, o16604, i141)
JMP1675(o859, o944, i184) → Load1265(o859, o944, i184)
NULL1315(o859, java.lang.Object(Tree(NULL, o944, o945)), i141, java.lang.Object(Tree(NULL, o944, o945))) → Load1265(o859, o944, i141 + 1)
NULL1315(java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950))) → Load22061(java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), NULL)
Store26568(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o18773, o18774, o18775)), o17144, o17145)), o16669, o18773) → Load22061(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(o18773, java.lang.Object(Tree(o18774, o17144, NULL)), NULL)), o16669)
Load22061(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o18773, o18774, o18775)), o17144, o17145)), o16669) → Load22061(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(o18773, java.lang.Object(Tree(o18774, o17144, NULL)), NULL)), o16669)
Load22061(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(NULL, o17144, o17145)), o16669) → Load22061(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), o17144, java.lang.Object(Tree(NULL, o16669, NULL)))
Load22061(java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), o16669) → Load22061(java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), java.lang.Object(Tree(o17890, java.lang.Object(Tree(o17891, o16672, NULL)), NULL)), o16669)
NULL1315(java.lang.Object(Tree(NULL, o949, o950)), java.lang.Object(Tree(NULL, o949, o950)), i141, java.lang.Object(Tree(NULL, o949, o950))) → JMP1675(java.lang.Object(Tree(NULL, o949, o950)), o949, i141 + 1)
Load22061(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o19695, o19696, o19697)), o17144, o17145)), o16669) → Store26568(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o19695, o19696, o19697)), o17144, o17145)), o16669, o19695)
The set Q consists of the following terms:
Load1265(x0, x1, x2)
NULL1315(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), x6, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)))
Store26273(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), x6, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), java.lang.Object(Tree(java.lang.Object(Tree(x7, x8, x9)), x10, x11)), x12, x7)
Load21911(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), x6, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), java.lang.Object(Tree(java.lang.Object(Tree(x7, x8, x9)), x10, x11)), x12)
Load21911(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), x6, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), java.lang.Object(Tree(NULL, x7, x8)), x9)
Load22061(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), x5, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), NULL, x6)
JMP22682(x0, x1, x2)
Load21911(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), x6, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), NULL, x7)
JMP1675(x0, x1, x2)
NULL1315(x0, java.lang.Object(Tree(NULL, x1, x2)), x3, java.lang.Object(Tree(NULL, x1, x2)))
Store26568(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), x5, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), x11, x6)
Load22061(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), x5, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), x11)
Load22061(java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), x5, java.lang.Object(Tree(java.lang.Object(Tree(x0, x1, x2)), x3, x4)), java.lang.Object(Tree(NULL, x6, x7)), x8)

(6) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

Store26568(x1, x2, x3, x4, x5, x6, x7) → Store26568(x3, x4, x5, x6, x7)
Load22061(x1, x2, x3, x4, x5, x6) → Load22061(x3, x4, x5, x6)
NULL1315(x1, x2, x3, x4) → NULL1315(x1, x3, x4)
Load21911(x1, x2, x3, x4, x5, x6) → Load21911(x1, x3, x4, x5, x6)
Store26273(x1, x2, x3, x4, x5, x6, x7) → Store26273(x1, x3, x4, x5, x6, x7)

(7) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load1265(o831, o830, i130) → NULL1315(o831, i130, o830)
NULL1315(o859, i141, java.lang.Object(Tree(java.lang.Object(Tree(o996Field0, o996Field1, o996Field2)), o944, o945))) → Load21911(o859, i141, java.lang.Object(Tree(java.lang.Object(Tree(o996Field0, o996Field1, o996Field2)), o944, o945)), java.lang.Object(Tree(java.lang.Object(Tree(o996Field0, o996Field1, o996Field2)), o944, o945)), NULL)
Store26273(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o18621, o18622, o18623)), o17126, o17127)), o16604, o18621) → Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(o18621, java.lang.Object(Tree(o18622, o17126, NULL)), NULL)), o16604)
Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o18621, o18622, o18623)), o17126, o17127)), o16604) → Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(o18621, java.lang.Object(Tree(o18622, o17126, NULL)), NULL)), o16604)
Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(NULL, o17126, o17127)), o16604) → Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), o17126, java.lang.Object(Tree(NULL, o16604, NULL)))
Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o17786, o17787, o17788)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o17786, o17787, o17788)), o16607, o16608)), o16604) → Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o17786, o17787, o17788)), o16607, o16608)), java.lang.Object(Tree(o17786, java.lang.Object(Tree(o17787, o16607, NULL)), NULL)), o16604)
Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o19480, o19481, o19482)), o17126, o17127)), o16604) → Store26273(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o19480, o19481, o19482)), o17126, o17127)), o16604, o19480)
Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), NULL, o16669) → JMP22682(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), o16669, i141)
JMP22682(o16609, o16604, i141) → Load1265(o16609, o16604, i141)
Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), NULL, o16604) → Load1265(o16609, o16604, i141)
JMP1675(o859, o944, i184) → Load1265(o859, o944, i184)
NULL1315(o859, i141, java.lang.Object(Tree(NULL, o944, o945))) → Load1265(o859, o944, i141 + 1)
NULL1315(java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950))) → Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), NULL)
Store26568(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o18773, o18774, o18775)), o17144, o17145)), o16669, o18773) → Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(o18773, java.lang.Object(Tree(o18774, o17144, NULL)), NULL)), o16669)
Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o18773, o18774, o18775)), o17144, o17145)), o16669) → Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(o18773, java.lang.Object(Tree(o18774, o17144, NULL)), NULL)), o16669)
Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(NULL, o17144, o17145)), o16669) → Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), o17144, java.lang.Object(Tree(NULL, o16669, NULL)))
Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), o16669) → Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), java.lang.Object(Tree(o17890, java.lang.Object(Tree(o17891, o16672, NULL)), NULL)), o16669)
NULL1315(java.lang.Object(Tree(NULL, o949, o950)), i141, java.lang.Object(Tree(NULL, o949, o950))) → JMP1675(java.lang.Object(Tree(NULL, o949, o950)), o949, i141 + 1)
Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o19695, o19696, o19697)), o17144, o17145)), o16669) → Store26568(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o19695, o19696, o19697)), o17144, o17145)), o16669, o19695)
The set Q consists of the following terms:
Load1265(x0, x1, x2)
NULL1315(x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x2, x3, x4)), x5, x6)))
Store26273(x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x2, x3, x4)), x5, x6)), java.lang.Object(Tree(java.lang.Object(Tree(x7, x8, x9)), x10, x11)), x12, x7)
Load21911(x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x2, x3, x4)), x5, x6)), java.lang.Object(Tree(java.lang.Object(Tree(x7, x8, x9)), x10, x11)), x12)
Load21911(x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x2, x3, x4)), x5, x6)), java.lang.Object(Tree(NULL, x7, x8)), x9)
Load22061(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), NULL, x6)
JMP22682(x0, x1, x2)
Load21911(x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x2, x3, x4)), x5, x6)), NULL, x7)
JMP1675(x0, x1, x2)
NULL1315(x0, x1, java.lang.Object(Tree(NULL, x2, x3)))
Store26568(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), x11, x6)
Load22061(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), x11)
Load22061(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), java.lang.Object(Tree(NULL, x6, x7)), x8)

(8) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(9) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
Load1265(o831, o830, i130) → NULL1315(o831, i130, o830)
NULL1315(o859, i141, java.lang.Object(Tree(java.lang.Object(Tree(o996Field0, o996Field1, o996Field2)), o944, o945))) → Load21911(o859, i141, java.lang.Object(Tree(java.lang.Object(Tree(o996Field0, o996Field1, o996Field2)), o944, o945)), java.lang.Object(Tree(java.lang.Object(Tree(o996Field0, o996Field1, o996Field2)), o944, o945)), NULL)
Store26273(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o18621, o18622, o18623)), o17126, o17127)), o16604, o18621) → Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(o18621, java.lang.Object(Tree(o18622, o17126, NULL)), NULL)), o16604)
Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o18621, o18622, o18623)), o17126, o17127)), o16604) → Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(o18621, java.lang.Object(Tree(o18622, o17126, NULL)), NULL)), o16604)
Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(NULL, o17126, o17127)), o16604) → Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), o17126, java.lang.Object(Tree(NULL, o16604, NULL)))
Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o17786, o17787, o17788)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o17786, o17787, o17788)), o16607, o16608)), o16604) → Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o17786, o17787, o17788)), o16607, o16608)), java.lang.Object(Tree(o17786, java.lang.Object(Tree(o17787, o16607, NULL)), NULL)), o16604)
Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o19480, o19481, o19482)), o17126, o17127)), o16604) → Store26273(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), java.lang.Object(Tree(java.lang.Object(Tree(o19480, o19481, o19482)), o17126, o17127)), o16604, o19480)
Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), NULL, o16669) → JMP22682(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), o16669, i141)
JMP22682(o16609, o16604, i141) → Load1265(o16609, o16604, i141)
Load21911(o16609, i141, java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0, o16606Field1, o16606Field2)), o16607, o16608)), NULL, o16604) → Load1265(o16609, o16604, i141)
JMP1675(o859, o944, i184) → Load1265(o859, o944, i184)
NULL1315(o859, i141, java.lang.Object(Tree(NULL, o944, o945))) → Load1265(o859, o944, i141 + 1)
NULL1315(java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), i141, java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950))) → Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0, o1010Field1, o1010Field2)), o949, o950)), NULL)
Store26568(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o18773, o18774, o18775)), o17144, o17145)), o16669, o18773) → Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(o18773, java.lang.Object(Tree(o18774, o17144, NULL)), NULL)), o16669)
Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o18773, o18774, o18775)), o17144, o17145)), o16669) → Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(o18773, java.lang.Object(Tree(o18774, o17144, NULL)), NULL)), o16669)
Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(NULL, o17144, o17145)), o16669) → Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), o17144, java.lang.Object(Tree(NULL, o16669, NULL)))
Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), o16669) → Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o17890, o17891, o17892)), o16672, o16673)), java.lang.Object(Tree(o17890, java.lang.Object(Tree(o17891, o16672, NULL)), NULL)), o16669)
NULL1315(java.lang.Object(Tree(NULL, o949, o950)), i141, java.lang.Object(Tree(NULL, o949, o950))) → JMP1675(java.lang.Object(Tree(NULL, o949, o950)), o949, i141 + 1)
Load22061(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o19695, o19696, o19697)), o17144, o17145)), o16669) → Store26568(i141, java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0, o16671Field1, o16671Field2)), o16672, o16673)), java.lang.Object(Tree(java.lang.Object(Tree(o19695, o19696, o19697)), o17144, o17145)), o16669, o19695)

The integer pair graph contains the following rules and edges:
(0): LOAD1265(o831[0], o830[0], i130[0]) → NULL1315'(o831[0], i130[0], o830[0])
(1): NULL1315'(o859[1], i141[1], java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1]))) → LOAD21911(o859[1], i141[1], java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])), java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])), NULL)
(2): STORE26273(o16609[2], i141[2], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[2], o16606Field1[2], o16606Field2[2])), o16607[2], o16608[2])), java.lang.Object(Tree(java.lang.Object(Tree(o18621[2], o18622[2], o18623[2])), o17126[2], o17127[2])), o16604[2], o18621[2]) → LOAD21911(o16609[2], i141[2], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[2], o16606Field1[2], o16606Field2[2])), o16607[2], o16608[2])), java.lang.Object(Tree(o18621[2], java.lang.Object(Tree(o18622[2], o17126[2], NULL)), NULL)), o16604[2])
(3): LOAD21911(o16609[3], i141[3], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])), java.lang.Object(Tree(java.lang.Object(Tree(o18621[3], o18622[3], o18623[3])), o17126[3], o17127[3])), o16604[3]) → LOAD21911(o16609[3], i141[3], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])), java.lang.Object(Tree(o18621[3], java.lang.Object(Tree(o18622[3], o17126[3], NULL)), NULL)), o16604[3])
(4): LOAD21911(o16609[4], i141[4], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])), java.lang.Object(Tree(NULL, o17126[4], o17127[4])), o16604[4]) → LOAD21911(o16609[4], i141[4], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])), o17126[4], java.lang.Object(Tree(NULL, o16604[4], NULL)))
(5): LOAD21911(o16609[5], i141[5], java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])), java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])), o16604[5]) → LOAD21911(o16609[5], i141[5], java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])), java.lang.Object(Tree(o17786[5], java.lang.Object(Tree(o17787[5], o16607[5], NULL)), NULL)), o16604[5])
(6): LOAD21911(o16609[6], i141[6], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[6], o16606Field1[6], o16606Field2[6])), o16607[6], o16608[6])), java.lang.Object(Tree(java.lang.Object(Tree(o19480[6], o19481[6], o19482[6])), o17126[6], o17127[6])), o16604[6]) → STORE26273(o16609[6], i141[6], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[6], o16606Field1[6], o16606Field2[6])), o16607[6], o16608[6])), java.lang.Object(Tree(java.lang.Object(Tree(o19480[6], o19481[6], o19482[6])), o17126[6], o17127[6])), o16604[6], o19480[6])
(7): LOAD22061(i141[7], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[7], o16671Field1[7], o16671Field2[7])), o16672[7], o16673[7])), NULL, o16669[7]) → JMP22682'(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[7], o16671Field1[7], o16671Field2[7])), o16672[7], o16673[7])), o16669[7], i141[7])
(8): JMP22682'(o16609[8], o16604[8], i141[8]) → LOAD1265(o16609[8], o16604[8], i141[8])
(9): LOAD21911(o16609[9], i141[9], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[9], o16606Field1[9], o16606Field2[9])), o16607[9], o16608[9])), NULL, o16604[9]) → LOAD1265(o16609[9], o16604[9], i141[9])
(10): JMP1675'(o859[10], o944[10], i184[10]) → LOAD1265(o859[10], o944[10], i184[10])
(11): NULL1315'(o859[11], i141[11], java.lang.Object(Tree(NULL, o944[11], o945[11]))) → LOAD1265(o859[11], o944[11], i141[11] + 1)
(12): NULL1315'(java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])), i141[12], java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12]))) → LOAD22061(i141[12], java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])), java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])), NULL)
(13): STORE26568(i141[13], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[13], o16671Field1[13], o16671Field2[13])), o16672[13], o16673[13])), java.lang.Object(Tree(java.lang.Object(Tree(o18773[13], o18774[13], o18775[13])), o17144[13], o17145[13])), o16669[13], o18773[13]) → LOAD22061(i141[13], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[13], o16671Field1[13], o16671Field2[13])), o16672[13], o16673[13])), java.lang.Object(Tree(o18773[13], java.lang.Object(Tree(o18774[13], o17144[13], NULL)), NULL)), o16669[13])
(14): LOAD22061(i141[14], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14])), java.lang.Object(Tree(java.lang.Object(Tree(o18773[14], o18774[14], o18775[14])), o17144[14], o17145[14])), o16669[14]) → LOAD22061(i141[14], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14])), java.lang.Object(Tree(o18773[14], java.lang.Object(Tree(o18774[14], o17144[14], NULL)), NULL)), o16669[14])
(15): LOAD22061(i141[15], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])), java.lang.Object(Tree(NULL, o17144[15], o17145[15])), o16669[15]) → LOAD22061(i141[15], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])), o17144[15], java.lang.Object(Tree(NULL, o16669[15], NULL)))
(16): LOAD22061(i141[16], java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])), java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])), o16669[16]) → LOAD22061(i141[16], java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])), java.lang.Object(Tree(o17890[16], java.lang.Object(Tree(o17891[16], o16672[16], NULL)), NULL)), o16669[16])
(17): NULL1315'(java.lang.Object(Tree(NULL, o949[17], o950[17])), i141[17], java.lang.Object(Tree(NULL, o949[17], o950[17]))) → JMP1675'(java.lang.Object(Tree(NULL, o949[17], o950[17])), o949[17], i141[17] + 1)
(18): LOAD22061(i141[18], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[18], o16671Field1[18], o16671Field2[18])), o16672[18], o16673[18])), java.lang.Object(Tree(java.lang.Object(Tree(o19695[18], o19696[18], o19697[18])), o17144[18], o17145[18])), o16669[18]) → STORE26568(i141[18], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[18], o16671Field1[18], o16671Field2[18])), o16672[18], o16673[18])), java.lang.Object(Tree(java.lang.Object(Tree(o19695[18], o19696[18], o19697[18])), o17144[18], o17145[18])), o16669[18], o19695[18])

(0) -> (1), if ((o830[0] →^* java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])))∧(o831[0] →^* o859[1])∧(i130[0] →^* i141[1]))

(0) -> (11), if ((o831[0] →^* o859[11])∧(o830[0] →^* java.lang.Object(Tree(NULL, o944[11], o945[11])))∧(i130[0] →^* i141[11]))

(0) -> (12), if ((o830[0] →^* java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])))∧(i130[0] →^* i141[12])∧(o831[0] →^* java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12]))))

(0) -> (17), if ((i130[0] →^* i141[17])∧(o830[0] →^* java.lang.Object(Tree(NULL, o949[17], o950[17])))∧(o831[0] →^* java.lang.Object(Tree(NULL, o949[17], o950[17]))))

(1) -> (3), if ((i141[1] →^* i141[3])∧(NULL →^* o16604[3])∧(o859[1] →^* o16609[3])∧(java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])))∧(java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o18621[3], o18622[3], o18623[3])), o17126[3], o17127[3]))))

(1) -> (4), if ((java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])) →^* java.lang.Object(Tree(NULL, o17126[4], o17127[4])))∧(NULL →^* o16604[4])∧(o859[1] →^* o16609[4])∧(java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])))∧(i141[1] →^* i141[4]))

(1) -> (5), if ((i141[1] →^* i141[5])∧(o859[1] →^* o16609[5])∧(java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])))∧(NULL →^* o16604[5]))

(1) -> (6), if ((NULL →^* o16604[6])∧(java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o19480[6], o19481[6], o19482[6])), o17126[6], o17127[6])))∧(o859[1] →^* o16609[6])∧(i141[1] →^* i141[6])∧(java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[6], o16606Field1[6], o16606Field2[6])), o16607[6], o16608[6]))))

(1) -> (9), if ((java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])) →^* NULL)∧(java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[9], o16606Field1[9], o16606Field2[9])), o16607[9], o16608[9])))∧(o859[1] →^* o16609[9])∧(NULL →^* o16604[9])∧(i141[1] →^* i141[9]))

(2) -> (3), if ((o16609[2] →^* o16609[3])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[2], o16606Field1[2], o16606Field2[2])), o16607[2], o16608[2])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])))∧(java.lang.Object(Tree(o18621[2], java.lang.Object(Tree(o18622[2], o17126[2], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o18621[3], o18622[3], o18623[3])), o17126[3], o17127[3])))∧(i141[2] →^* i141[3])∧(o16604[2] →^* o16604[3]))

(2) -> (4), if ((o16604[2] →^* o16604[4])∧(java.lang.Object(Tree(o18621[2], java.lang.Object(Tree(o18622[2], o17126[2], NULL)), NULL)) →^* java.lang.Object(Tree(NULL, o17126[4], o17127[4])))∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[2], o16606Field1[2], o16606Field2[2])), o16607[2], o16608[2])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])))∧(o16609[2] →^* o16609[4])∧(i141[2] →^* i141[4]))

(2) -> (5), if ((java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[2], o16606Field1[2], o16606Field2[2])), o16607[2], o16608[2])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])))∧(o16609[2] →^* o16609[5])∧(o16604[2] →^* o16604[5])∧(i141[2] →^* i141[5])∧(java.lang.Object(Tree(o18621[2], java.lang.Object(Tree(o18622[2], o17126[2], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5]))))

(2) -> (6), if ((o16609[2] →^* o16609[6])∧(o16604[2] →^* o16604[6])∧(java.lang.Object(Tree(o18621[2], java.lang.Object(Tree(o18622[2], o17126[2], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o19480[6], o19481[6], o19482[6])), o17126[6], o17127[6])))∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[2], o16606Field1[2], o16606Field2[2])), o16607[2], o16608[2])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[6], o16606Field1[6], o16606Field2[6])), o16607[6], o16608[6])))∧(i141[2] →^* i141[6]))

(2) -> (9), if ((java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[2], o16606Field1[2], o16606Field2[2])), o16607[2], o16608[2])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[9], o16606Field1[9], o16606Field2[9])), o16607[9], o16608[9])))∧(o16609[2] →^* o16609[9])∧(i141[2] →^* i141[9])∧(o16604[2] →^* o16604[9])∧(java.lang.Object(Tree(o18621[2], java.lang.Object(Tree(o18622[2], o17126[2], NULL)), NULL)) →^* NULL))

(3) -> (3), if ((java.lang.Object(Tree(o18621[3], java.lang.Object(Tree(o18622[3], o17126[3], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o18621[3]', o18622[3]', o18623[3]')), o17126[3]', o17127[3]')))∧(o16609[3] →^* o16609[3]')∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3]', o16606Field1[3]', o16606Field2[3]')), o16607[3]', o16608[3]')))∧(i141[3] →^* i141[3]')∧(o16604[3] →^* o16604[3]'))

(3) -> (4), if ((o16609[3] →^* o16609[4])∧(java.lang.Object(Tree(o18621[3], java.lang.Object(Tree(o18622[3], o17126[3], NULL)), NULL)) →^* java.lang.Object(Tree(NULL, o17126[4], o17127[4])))∧(i141[3] →^* i141[4])∧(o16604[3] →^* o16604[4])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4]))))

(3) -> (5), if ((o16604[3] →^* o16604[5])∧(i141[3] →^* i141[5])∧(java.lang.Object(Tree(o18621[3], java.lang.Object(Tree(o18622[3], o17126[3], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])))∧(o16609[3] →^* o16609[5])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5]))))

(3) -> (6), if ((o16609[3] →^* o16609[6])∧(java.lang.Object(Tree(o18621[3], java.lang.Object(Tree(o18622[3], o17126[3], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o19480[6], o19481[6], o19482[6])), o17126[6], o17127[6])))∧(i141[3] →^* i141[6])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[6], o16606Field1[6], o16606Field2[6])), o16607[6], o16608[6])))∧(o16604[3] →^* o16604[6]))

(3) -> (9), if ((java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[9], o16606Field1[9], o16606Field2[9])), o16607[9], o16608[9])))∧(java.lang.Object(Tree(o18621[3], java.lang.Object(Tree(o18622[3], o17126[3], NULL)), NULL)) →^* NULL)∧(o16604[3] →^* o16604[9])∧(o16609[3] →^* o16609[9])∧(i141[3] →^* i141[9]))

(4) -> (3), if ((i141[4] →^* i141[3])∧(o16609[4] →^* o16609[3])∧(java.lang.Object(Tree(NULL, o16604[4], NULL)) →^* o16604[3])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])))∧(o17126[4] →^* java.lang.Object(Tree(java.lang.Object(Tree(o18621[3], o18622[3], o18623[3])), o17126[3], o17127[3]))))

(4) -> (4), if ((java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4]', o16606Field1[4]', o16606Field2[4]')), o16607[4]', o16608[4]')))∧(o17126[4] →^* java.lang.Object(Tree(NULL, o17126[4]', o17127[4]')))∧(java.lang.Object(Tree(NULL, o16604[4], NULL)) →^* o16604[4]')∧(i141[4] →^* i141[4]')∧(o16609[4] →^* o16609[4]'))

(4) -> (5), if ((java.lang.Object(Tree(NULL, o16604[4], NULL)) →^* o16604[5])∧(i141[4] →^* i141[5])∧(o16609[4] →^* o16609[5])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])))∧(o17126[4] →^* java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5]))))

(4) -> (6), if ((i141[4] →^* i141[6])∧(o17126[4] →^* java.lang.Object(Tree(java.lang.Object(Tree(o19480[6], o19481[6], o19482[6])), o17126[6], o17127[6])))∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[6], o16606Field1[6], o16606Field2[6])), o16607[6], o16608[6])))∧(java.lang.Object(Tree(NULL, o16604[4], NULL)) →^* o16604[6])∧(o16609[4] →^* o16609[6]))

(4) -> (9), if ((java.lang.Object(Tree(NULL, o16604[4], NULL)) →^* o16604[9])∧(o17126[4] →^* NULL)∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[9], o16606Field1[9], o16606Field2[9])), o16607[9], o16608[9])))∧(i141[4] →^* i141[9])∧(o16609[4] →^* o16609[9]))

(5) -> (3), if ((java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])))∧(java.lang.Object(Tree(o17786[5], java.lang.Object(Tree(o17787[5], o16607[5], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o18621[3], o18622[3], o18623[3])), o17126[3], o17127[3])))∧(o16609[5] →^* o16609[3])∧(o16604[5] →^* o16604[3])∧(i141[5] →^* i141[3]))

(5) -> (4), if ((i141[5] →^* i141[4])∧(java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])))∧(o16609[5] →^* o16609[4])∧(o16604[5] →^* o16604[4])∧(java.lang.Object(Tree(o17786[5], java.lang.Object(Tree(o17787[5], o16607[5], NULL)), NULL)) →^* java.lang.Object(Tree(NULL, o17126[4], o17127[4]))))

(5) -> (5), if ((o16609[5] →^* o16609[5]')∧(java.lang.Object(Tree(o17786[5], java.lang.Object(Tree(o17787[5], o16607[5], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17786[5]', o17787[5]', o17788[5]')), o16607[5]', o16608[5]')))∧(java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17786[5]', o17787[5]', o17788[5]')), o16607[5]', o16608[5]')))∧(i141[5] →^* i141[5]')∧(o16604[5] →^* o16604[5]'))

(5) -> (6), if ((o16609[5] →^* o16609[6])∧(java.lang.Object(Tree(o17786[5], java.lang.Object(Tree(o17787[5], o16607[5], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o19480[6], o19481[6], o19482[6])), o17126[6], o17127[6])))∧(i141[5] →^* i141[6])∧(o16604[5] →^* o16604[6])∧(java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[6], o16606Field1[6], o16606Field2[6])), o16607[6], o16608[6]))))

(5) -> (9), if ((o16604[5] →^* o16604[9])∧(o16609[5] →^* o16609[9])∧(java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[9], o16606Field1[9], o16606Field2[9])), o16607[9], o16608[9])))∧(java.lang.Object(Tree(o17786[5], java.lang.Object(Tree(o17787[5], o16607[5], NULL)), NULL)) →^* NULL)∧(i141[5] →^* i141[9]))

(6) -> (2), if ((o16609[6] →^* o16609[2])∧(java.lang.Object(Tree(java.lang.Object(Tree(o19480[6], o19481[6], o19482[6])), o17126[6], o17127[6])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o18621[2], o18622[2], o18623[2])), o17126[2], o17127[2])))∧(o16604[6] →^* o16604[2])∧(i141[6] →^* i141[2])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[6], o16606Field1[6], o16606Field2[6])), o16607[6], o16608[6])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[2], o16606Field1[2], o16606Field2[2])), o16607[2], o16608[2])))∧(o19480[6] →^* o18621[2]))

(7) -> (8), if ((o16669[7] →^* o16604[8])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[7], o16671Field1[7], o16671Field2[7])), o16672[7], o16673[7])) →^* o16609[8])∧(i141[7] →^* i141[8]))

(8) -> (0), if ((o16604[8] →^* o830[0])∧(o16609[8] →^* o831[0])∧(i141[8] →^* i130[0]))

(9) -> (0), if ((o16604[9] →^* o830[0])∧(o16609[9] →^* o831[0])∧(i141[9] →^* i130[0]))

(10) -> (0), if ((i184[10] →^* i130[0])∧(o944[10] →^* o830[0])∧(o859[10] →^* o831[0]))

(11) -> (0), if ((i141[11] + 1 →^* i130[0])∧(o944[11] →^* o830[0])∧(o859[11] →^* o831[0]))

(12) -> (7), if ((java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])) →^* NULL)∧(NULL →^* o16669[7])∧(java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[7], o16671Field1[7], o16671Field2[7])), o16672[7], o16673[7])))∧(i141[12] →^* i141[7]))

(12) -> (14), if ((java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o18773[14], o18774[14], o18775[14])), o17144[14], o17145[14])))∧(NULL →^* o16669[14])∧(java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14])))∧(i141[12] →^* i141[14]))

(12) -> (15), if ((NULL →^* o16669[15])∧(java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])))∧(i141[12] →^* i141[15])∧(java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])) →^* java.lang.Object(Tree(NULL, o17144[15], o17145[15]))))

(12) -> (16), if ((java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])))∧(i141[12] →^* i141[16])∧(NULL →^* o16669[16]))

(12) -> (18), if ((java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o19695[18], o19696[18], o19697[18])), o17144[18], o17145[18])))∧(i141[12] →^* i141[18])∧(java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[18], o16671Field1[18], o16671Field2[18])), o16672[18], o16673[18])))∧(NULL →^* o16669[18]))

(13) -> (7), if ((o16669[13] →^* o16669[7])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[13], o16671Field1[13], o16671Field2[13])), o16672[13], o16673[13])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[7], o16671Field1[7], o16671Field2[7])), o16672[7], o16673[7])))∧(java.lang.Object(Tree(o18773[13], java.lang.Object(Tree(o18774[13], o17144[13], NULL)), NULL)) →^* NULL)∧(i141[13] →^* i141[7]))

(13) -> (14), if ((i141[13] →^* i141[14])∧(java.lang.Object(Tree(o18773[13], java.lang.Object(Tree(o18774[13], o17144[13], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o18773[14], o18774[14], o18775[14])), o17144[14], o17145[14])))∧(o16669[13] →^* o16669[14])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[13], o16671Field1[13], o16671Field2[13])), o16672[13], o16673[13])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14]))))

(13) -> (15), if ((java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[13], o16671Field1[13], o16671Field2[13])), o16672[13], o16673[13])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])))∧(o16669[13] →^* o16669[15])∧(i141[13] →^* i141[15])∧(java.lang.Object(Tree(o18773[13], java.lang.Object(Tree(o18774[13], o17144[13], NULL)), NULL)) →^* java.lang.Object(Tree(NULL, o17144[15], o17145[15]))))

(13) -> (16), if ((java.lang.Object(Tree(o18773[13], java.lang.Object(Tree(o18774[13], o17144[13], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])))∧(i141[13] →^* i141[16])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[13], o16671Field1[13], o16671Field2[13])), o16672[13], o16673[13])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])))∧(o16669[13] →^* o16669[16]))

(13) -> (18), if ((i141[13] →^* i141[18])∧(o16669[13] →^* o16669[18])∧(java.lang.Object(Tree(o18773[13], java.lang.Object(Tree(o18774[13], o17144[13], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o19695[18], o19696[18], o19697[18])), o17144[18], o17145[18])))∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[13], o16671Field1[13], o16671Field2[13])), o16672[13], o16673[13])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[18], o16671Field1[18], o16671Field2[18])), o16672[18], o16673[18]))))

(14) -> (7), if ((o16669[14] →^* o16669[7])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[7], o16671Field1[7], o16671Field2[7])), o16672[7], o16673[7])))∧(java.lang.Object(Tree(o18773[14], java.lang.Object(Tree(o18774[14], o17144[14], NULL)), NULL)) →^* NULL)∧(i141[14] →^* i141[7]))

(14) -> (14), if ((java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14]', o16671Field1[14]', o16671Field2[14]')), o16672[14]', o16673[14]')))∧(o16669[14] →^* o16669[14]')∧(java.lang.Object(Tree(o18773[14], java.lang.Object(Tree(o18774[14], o17144[14], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o18773[14]', o18774[14]', o18775[14]')), o17144[14]', o17145[14]')))∧(i141[14] →^* i141[14]'))

(14) -> (15), if ((o16669[14] →^* o16669[15])∧(i141[14] →^* i141[15])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])))∧(java.lang.Object(Tree(o18773[14], java.lang.Object(Tree(o18774[14], o17144[14], NULL)), NULL)) →^* java.lang.Object(Tree(NULL, o17144[15], o17145[15]))))

(14) -> (16), if ((o16669[14] →^* o16669[16])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])))∧(java.lang.Object(Tree(o18773[14], java.lang.Object(Tree(o18774[14], o17144[14], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])))∧(i141[14] →^* i141[16]))

(14) -> (18), if ((i141[14] →^* i141[18])∧(java.lang.Object(Tree(o18773[14], java.lang.Object(Tree(o18774[14], o17144[14], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o19695[18], o19696[18], o19697[18])), o17144[18], o17145[18])))∧(o16669[14] →^* o16669[18])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[18], o16671Field1[18], o16671Field2[18])), o16672[18], o16673[18]))))

(15) -> (7), if ((o17144[15] →^* NULL)∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[7], o16671Field1[7], o16671Field2[7])), o16672[7], o16673[7])))∧(java.lang.Object(Tree(NULL, o16669[15], NULL)) →^* o16669[7])∧(i141[15] →^* i141[7]))

(15) -> (14), if ((o17144[15] →^* java.lang.Object(Tree(java.lang.Object(Tree(o18773[14], o18774[14], o18775[14])), o17144[14], o17145[14])))∧(java.lang.Object(Tree(NULL, o16669[15], NULL)) →^* o16669[14])∧(i141[15] →^* i141[14])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14]))))

(15) -> (15), if ((java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15]', o16671Field1[15]', o16671Field2[15]')), o16672[15]', o16673[15]')))∧(java.lang.Object(Tree(NULL, o16669[15], NULL)) →^* o16669[15]')∧(o17144[15] →^* java.lang.Object(Tree(NULL, o17144[15]', o17145[15]')))∧(i141[15] →^* i141[15]'))

(15) -> (16), if ((java.lang.Object(Tree(NULL, o16669[15], NULL)) →^* o16669[16])∧(o17144[15] →^* java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])))∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])))∧(i141[15] →^* i141[16]))

(15) -> (18), if ((i141[15] →^* i141[18])∧(java.lang.Object(Tree(NULL, o16669[15], NULL)) →^* o16669[18])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[18], o16671Field1[18], o16671Field2[18])), o16672[18], o16673[18])))∧(o17144[15] →^* java.lang.Object(Tree(java.lang.Object(Tree(o19695[18], o19696[18], o19697[18])), o17144[18], o17145[18]))))

(16) -> (7), if ((java.lang.Object(Tree(o17890[16], java.lang.Object(Tree(o17891[16], o16672[16], NULL)), NULL)) →^* NULL)∧(i141[16] →^* i141[7])∧(java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[7], o16671Field1[7], o16671Field2[7])), o16672[7], o16673[7])))∧(o16669[16] →^* o16669[7]))

(16) -> (14), if ((java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14])))∧(java.lang.Object(Tree(o17890[16], java.lang.Object(Tree(o17891[16], o16672[16], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o18773[14], o18774[14], o18775[14])), o17144[14], o17145[14])))∧(o16669[16] →^* o16669[14])∧(i141[16] →^* i141[14]))

(16) -> (15), if ((i141[16] →^* i141[15])∧(java.lang.Object(Tree(o17890[16], java.lang.Object(Tree(o17891[16], o16672[16], NULL)), NULL)) →^* java.lang.Object(Tree(NULL, o17144[15], o17145[15])))∧(o16669[16] →^* o16669[15])∧(java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15]))))

(16) -> (16), if ((java.lang.Object(Tree(o17890[16], java.lang.Object(Tree(o17891[16], o16672[16], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17890[16]', o17891[16]', o17892[16]')), o16672[16]', o16673[16]')))∧(java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o17890[16]', o17891[16]', o17892[16]')), o16672[16]', o16673[16]')))∧(o16669[16] →^* o16669[16]')∧(i141[16] →^* i141[16]'))

(16) -> (18), if ((java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[18], o16671Field1[18], o16671Field2[18])), o16672[18], o16673[18])))∧(java.lang.Object(Tree(o17890[16], java.lang.Object(Tree(o17891[16], o16672[16], NULL)), NULL)) →^* java.lang.Object(Tree(java.lang.Object(Tree(o19695[18], o19696[18], o19697[18])), o17144[18], o17145[18])))∧(i141[16] →^* i141[18])∧(o16669[16] →^* o16669[18]))

(17) -> (10), if ((java.lang.Object(Tree(NULL, o949[17], o950[17])) →^* o859[10])∧(o949[17] →^* o944[10])∧(i141[17] + 1 →^* i184[10]))

(18) -> (13), if ((o19695[18] →^* o18773[13])∧(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[18], o16671Field1[18], o16671Field2[18])), o16672[18], o16673[18])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[13], o16671Field1[13], o16671Field2[13])), o16672[13], o16673[13])))∧(i141[18] →^* i141[13])∧(o16669[18] →^* o16669[13])∧(java.lang.Object(Tree(java.lang.Object(Tree(o19695[18], o19696[18], o19697[18])), o17144[18], o17145[18])) →^* java.lang.Object(Tree(java.lang.Object(Tree(o18773[13], o18774[13], o18775[13])), o17144[13], o17145[13]))))

The set Q consists of the following terms:
Load1265(x0, x1, x2)
NULL1315(x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x2, x3, x4)), x5, x6)))
Store26273(x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x2, x3, x4)), x5, x6)), java.lang.Object(Tree(java.lang.Object(Tree(x7, x8, x9)), x10, x11)), x12, x7)
Load21911(x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x2, x3, x4)), x5, x6)), java.lang.Object(Tree(java.lang.Object(Tree(x7, x8, x9)), x10, x11)), x12)
Load21911(x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x2, x3, x4)), x5, x6)), java.lang.Object(Tree(NULL, x7, x8)), x9)
Load22061(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), NULL, x6)
JMP22682(x0, x1, x2)
Load21911(x0, x1, java.lang.Object(Tree(java.lang.Object(Tree(x2, x3, x4)), x5, x6)), NULL, x7)
JMP1675(x0, x1, x2)
NULL1315(x0, x1, java.lang.Object(Tree(NULL, x2, x3)))
Store26568(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), x11, x6)
Load22061(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), java.lang.Object(Tree(java.lang.Object(Tree(x6, x7, x8)), x9, x10)), x11)
Load22061(x0, java.lang.Object(Tree(java.lang.Object(Tree(x1, x2, x3)), x4, x5)), java.lang.Object(Tree(NULL, x6, x7)), x8)

(10) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD1265(o831[0], o830[0], i130[0]) → NULL1315'(o831[0], i130[0], o830[0])
(1): NULL1315'(o859[1], i141[1], java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1]))) → LOAD21911(o859[1], i141[1], java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])), java.lang.Object(Tree(java.lang.Object(Tree(o996Field0[1], o996Field1[1], o996Field2[1])), o944[1], o945[1])), NULL)
(2): STORE26273(o16609[2], i141[2], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[2], o16606Field1[2], o16606Field2[2])), o16607[2], o16608[2])), java.lang.Object(Tree(java.lang.Object(Tree(o18621[2], o18622[2], o18623[2])), o17126[2], o17127[2])), o16604[2], o18621[2]) → LOAD21911(o16609[2], i141[2], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[2], o16606Field1[2], o16606Field2[2])), o16607[2], o16608[2])), java.lang.Object(Tree(o18621[2], java.lang.Object(Tree(o18622[2], o17126[2], NULL)), NULL)), o16604[2])
(3): LOAD21911(o16609[3], i141[3], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])), java.lang.Object(Tree(java.lang.Object(Tree(o18621[3], o18622[3], o18623[3])), o17126[3], o17127[3])), o16604[3]) → LOAD21911(o16609[3], i141[3], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[3], o16606Field1[3], o16606Field2[3])), o16607[3], o16608[3])), java.lang.Object(Tree(o18621[3], java.lang.Object(Tree(o18622[3], o17126[3], NULL)), NULL)), o16604[3])
(4): LOAD21911(o16609[4], i141[4], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])), java.lang.Object(Tree(NULL, o17126[4], o17127[4])), o16604[4]) → LOAD21911(o16609[4], i141[4], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[4], o16606Field1[4], o16606Field2[4])), o16607[4], o16608[4])), o17126[4], java.lang.Object(Tree(NULL, o16604[4], NULL)))
(5): LOAD21911(o16609[5], i141[5], java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])), java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])), o16604[5]) → LOAD21911(o16609[5], i141[5], java.lang.Object(Tree(java.lang.Object(Tree(o17786[5], o17787[5], o17788[5])), o16607[5], o16608[5])), java.lang.Object(Tree(o17786[5], java.lang.Object(Tree(o17787[5], o16607[5], NULL)), NULL)), o16604[5])
(6): LOAD21911(o16609[6], i141[6], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[6], o16606Field1[6], o16606Field2[6])), o16607[6], o16608[6])), java.lang.Object(Tree(java.lang.Object(Tree(o19480[6], o19481[6], o19482[6])), o17126[6], o17127[6])), o16604[6]) → STORE26273(o16609[6], i141[6], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[6], o16606Field1[6], o16606Field2[6])), o16607[6], o16608[6])), java.lang.Object(Tree(java.lang.Object(Tree(o19480[6], o19481[6], o19482[6])), o17126[6], o17127[6])), o16604[6], o19480[6])
(7): LOAD22061(i141[7], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[7], o16671Field1[7], o16671Field2[7])), o16672[7], o16673[7])), NULL, o16669[7]) → JMP22682'(java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[7], o16671Field1[7], o16671Field2[7])), o16672[7], o16673[7])), o16669[7], i141[7])
(8): JMP22682'(o16609[8], o16604[8], i141[8]) → LOAD1265(o16609[8], o16604[8], i141[8])
(9): LOAD21911(o16609[9], i141[9], java.lang.Object(Tree(java.lang.Object(Tree(o16606Field0[9], o16606Field1[9], o16606Field2[9])), o16607[9], o16608[9])), NULL, o16604[9]) → LOAD1265(o16609[9], o16604[9], i141[9])
(10): JMP1675'(o859[10], o944[10], i184[10]) → LOAD1265(o859[10], o944[10], i184[10])
(11): NULL1315'(o859[11], i141[11], java.lang.Object(Tree(NULL, o944[11], o945[11]))) → LOAD1265(o859[11], o944[11], i141[11] + 1)
(12): NULL1315'(java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])), i141[12], java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12]))) → LOAD22061(i141[12], java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])), java.lang.Object(Tree(java.lang.Object(Tree(o1010Field0[12], o1010Field1[12], o1010Field2[12])), o949[12], o950[12])), NULL)
(13): STORE26568(i141[13], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[13], o16671Field1[13], o16671Field2[13])), o16672[13], o16673[13])), java.lang.Object(Tree(java.lang.Object(Tree(o18773[13], o18774[13], o18775[13])), o17144[13], o17145[13])), o16669[13], o18773[13]) → LOAD22061(i141[13], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[13], o16671Field1[13], o16671Field2[13])), o16672[13], o16673[13])), java.lang.Object(Tree(o18773[13], java.lang.Object(Tree(o18774[13], o17144[13], NULL)), NULL)), o16669[13])
(14): LOAD22061(i141[14], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14])), java.lang.Object(Tree(java.lang.Object(Tree(o18773[14], o18774[14], o18775[14])), o17144[14], o17145[14])), o16669[14]) → LOAD22061(i141[14], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[14], o16671Field1[14], o16671Field2[14])), o16672[14], o16673[14])), java.lang.Object(Tree(o18773[14], java.lang.Object(Tree(o18774[14], o17144[14], NULL)), NULL)), o16669[14])
(15): LOAD22061(i141[15], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])), java.lang.Object(Tree(NULL, o17144[15], o17145[15])), o16669[15]) → LOAD22061(i141[15], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[15], o16671Field1[15], o16671Field2[15])), o16672[15], o16673[15])), o17144[15], java.lang.Object(Tree(NULL, o16669[15], NULL)))
(16): LOAD22061(i141[16], java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])), java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])), o16669[16]) → LOAD22061(i141[16], java.lang.Object(Tree(java.lang.Object(Tree(o17890[16], o17891[16], o17892[16])), o16672[16], o16673[16])), java.lang.Object(Tree(o17890[16], java.lang.Object(Tree(o17891[16], o16672[16], NULL)), NULL)), o16669[16])
(17): NULL1315'(java.lang.Object(Tree(NULL, o949[17], o950[17])), i141[17], java.lang.Object(Tree(NULL, o949[17], o950[17]))) → JMP1675'(java.lang.Object(Tree(NULL, o949[17], o950[17])), o949[17], i141[17] + 1)
(18): LOAD22061(i141[18], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[18], o16671Field1[18], o16671Field2[18])), o16672[18], o16673[18])), java.lang.Object(Tree(java.lang.Object(Tree(o19695[18], o19696[18], o19697[18])), o17144[18], o17145[18])), o16669[18]) → STORE26568(i141[18], java.lang.Object(Tree(java.lang.Object(Tree(o16671Field0[18], o16671Field1[18], o16671Field2[18])), o16672[18], o16673[18])), java.lang.Object(Tree(java.lang.Object(Tree(o19695[18], o19696[18], o19697[18])), o17144[18], o17145[18])), o16669[18], o19695[18])